| Definitions | False, #$n,  b, (i = j), qeq(r; s), ff, tt, <a, b>,  , s = t, inl x , if b then t else f fi , qle(r; s), l_all(L; T; x.P(x)), t  T, x:A  B(x), P   Q,  x:A. B(x), P  Q, x:A  B(x), rationals, P  Q, P Q, x f y, i <z j, rng_zero(r), qrng, rng_plus(r), grp_id(g), add_grp_of_rng(r), grp_op(g), mon_itop(g; lb; ub; i.E(i)), rng_sum(r; i; j; k.E(k)), qsum(a; b; j.E(j)), guard(T), sq_type(T), sqequal(s; t), type List, {x:A| B(x)} , finite-prob-space |